\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:Id, $T$:Type, ${\it ks}$:(Knd List),\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]($\neg$($\uparrow$fpf{-}dom(id{-}deq; $x$; ${\it ds}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$A$:es\_realizer\{i:l\}. \+
\\[0ex]R{-}Feasible\=\{i:l\}\+
\\[0ex]($A$)
\-\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$R{-}occurs($A$; $i$; $x$)))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}$; R{-}ds($A$; $i$))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Knd; $k$.Type; Kind{-}deq; ${\it da}$; R{-}da($A$; $i$))
\\[0ex]$\Rightarrow$ l\_all(\=${\it ks}$;\+
\\[0ex]Knd;
\\[0ex]$k$.(($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ subtype\_rel(\=fpf{-}cap(R{-}da($A$; source(lnk($k$))); Kind{-}deq; $k$; void);\+
\\[0ex]ma{-}valtype(${\it da}$; $k$))))
\-\-\\[0ex]$\Rightarrow$ l\_all(${\it ks}$; Knd; $k$.($\uparrow$fpf{-}dom(Kind{-}deq; $k$; ${\it da}$)))
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ ($\neg$($\uparrow$write{-}restricted($A$; $i$; $k$))))
\\[0ex]$\Rightarrow$ \=($\forall$$y$:Id. \+
\\[0ex]($\uparrow$fpf{-}dom(id{-}deq; $y$; fpf{-}join(id{-}deq; ${\it ds}$; fpf{-}single($x$; $T$))))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$read{-}restricted($A$; $i$; $y$))))
\-\\[0ex]$\Rightarrow$ R{-}compat\=\{i:l\}\+
\\[0ex](R{-}state{-}var($i$; ${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; ${\it tr}$); $A$))
\-\-
\end{tabbing}